package joc.nextgen;

import static joc.nextgen.JOC.old;
import static joc.nextgen.JOC.post;
import static joc.nextgen.JOC.pre;
import static joc.nextgen.JOC.result;

public class StackSpecContract<T> implements StackSpec<T> {
	@Override
	public int size() {
		if (post()) {
			assert result(Integer.class) >= 0;
		}
		return 0; // notwendig wegen implements
	}

	@Override
	public void pop() {
		if (pre()) {
			assert size() > 0;
		}
		if (post()) {
			assert size() == old(size()) - 1;
			assert top() == old(get(2));
		}
	}

	@Override
	public T get(int i) {
		if (pre()) {
			assert !isEmpty();
			assert i > 0;
			assert size() >= i;
		}
		if (post()) {
			assert result() != null;
		}
		return null;
	}

	@Override
	public boolean isFull() {
		return false;
	}

	@Override
	public boolean isEmpty() {
		return false;
	}

	@Override
	public T top() {
		if (pre()) {
			assert size() > 0;
		}
		if (post()) {
			assert size() == old(size());
		}
		return null;
	}

	@Override
	public void push(T elem) {
		if (pre()) {
			assert !isFull();
		}
		if (post()) {
			assert size() == old(size()) + 1;
			assert top() == elem;
		}
	}
}